Symbolic simulation is a well-known technology for the functional verification of digital circuits. Symbolic simulation differs from conventional simulation in that in conventional simulation programs both the inputs and outputs are actual binary values (1s and 0s)), whereas in symbolic simulation programs the inputs are symbols representing both 0 and 1 (e.g., a1, a2, a3, a4, . . . b1, b2, b3, b4, etc.) and the outputs are Boolean expressions. Typically the clock remains binary. The circuit is verified by checking the output Boolean expressions against a reference.
Some primarily digital circuits contain analog devices and hence have non-digital node voltages. The presence of analog devices in the circuit impacts the functionality being verified. For example, in normal digital simulation programs the output of the Schmitt trigger shown in FIG. 1 can only take on digital values, which means that the feedback transistors 10 and 12 appear to be either on or off. If transistors 10 and 12 are sized such that they are stronger than the other transistors in the device, then the current state of the output node will be permanently locked. In reality, however, when the input node switches from 1 to 0 or vice-versa, the voltage at the output node will shift slightly. This sets up a positive feedback condition that will end up with the output node completely shifted. This result can be accounted for, however, only if the voltage at the output node is capable of taking on non-digital voltages.
Similarly, with the sense-amplifier shown in FIG. 2, when the enable signal goes high, the voltages at “ti” and “tf” are isolated from the voltages at “t” and “f”, respectively, setting up a positive feedback condition that will result in the higher of “ti” and “tf” being pulled up to the supply voltage and the lower of “ti” and “tf” being pulled down to ground. In a digital simulation scheme, the node values can only be 1 or 0. Therefore, if t=1.5V and f=1.2V, both nodes will be represented as logical 1s. When the enable signal goes high an oscillation will be set up that will never resolve itself.
One way of dealing with this problem is to manually replace the analog devices in the circuit with digital models before verification. This process is time consuming and error prone, however, and therefore makes the accuracy of the results questionable.
Another technique for analyzing analog devices in digital circuits involves symbolic analysis in Mathematica™, using algebraic expressions that fully describe the behavior of the circuit. This is very slow, however, and is applicable only to very small circuits. Model-checking on extracted flow-graphs is similarly a very slow, manual effort. Use of SPICE or fast-Spice (Nanosim™, Hsim™, etc,) requires exhaustive test benches; the size of test bench increases exponentially with the size of the circuit being analyzed.
Accordingly, there is a clear need for a fast, efficient and accurate way of symbolically simulating and verifying digital circuits that contain analog components.